package datatableaux;

import kb.TBox;
import kb.SimpleReasoning;


import java.util.*;


import domain.*;
import entities.*;
import entities.concept.Concept;
import entities.concept.DomainConcept;
import entities.concept.NotConcept;
import entities.concept.PConcept;
/**
 *
 * Given a node, or a set of nodes, decide if any clash exists in the nodes.
 * f<g, g<f ->clash
 * k1<f, f<k2 -> decide if k1<k2?
 * f=k1, f=k2, k1!=k2 ->clash
 * 
 * @author j55wu
 *
 */
public class ClashTrigger {

	TBox tb;
	SimpleReasoning sr;
	
	public ClashTrigger(TBox tb){
		this.tb = tb;
		sr = new SimpleReasoning(this.tb);
	}
	
//	public boolean clashFound(Node n){
//		boolean clash = false;
//		if(n.getLabels().size()<1){
//			System.out.println("No concepts found in this node's label.");
//			return clash;
//		}
//		//return clashInLabels(preprocessor.Simplification.NNF(n.getLabels()));
//		return clashInLabels(n.getLabels());
//	}
	
	public boolean clashFound(Individual ind){
		boolean clash = false;
		if(ind.getLabels().size()<1){
			//System.out.println("No concepts found in this individual's label.");
			return clash;
		}
		//return clashInLabels(preprocessor.Simplification.NNF(n.getLabels()));
		return clashInLabels(ind.getLabels());
	}
	
	//true if there is a contradiction!
	public boolean clashInLabels(HashSet<Concept> cs){
		boolean clashfound = false;
		//for a set, test if all A super classes and all ~B subclasses are disjoint.
		HashSet<Concept> positives = new HashSet<Concept>();
		HashSet<Concept> negatives = new HashSet<Concept>();
		HashSet<DomainConcept<?,?>> ds = new HashSet<DomainConcept<?,?>>();
		for(Concept c:cs){
			//in case we have top/bot in our language
			if(c instanceof PConcept && c.isBot()){
				clashfound = true;
				return clashfound;
			}
			
			if(c instanceof NotConcept){
				//????A potential problem: what if the formulas are not in NNF, e.g., ~~~A?
				NotConcept nc = (NotConcept)c;
				Concept cnc = nc.getConcept();
				if(cnc instanceof PConcept && cnc.isTop()){
					clashfound = true;
					return clashfound;
				}
				//get all subclasses of cnc, as A->B, implies that ~B->~A
				negatives.addAll(sr.givenSubclasses(cnc));
			}else if(c instanceof DomainConcept){
				ds.add((DomainConcept<?,?>)c);
			}
			else{
				positives.addAll(sr.givenSuperclasses(c));
			}						
		}
		//Test whether clashes exist.
		clashfound |= !Collections.disjoint(positives, negatives);
		if(ds.size()>= 1){
			//if only one, not need to test -> always sat
			clashfound |= this.clashConcreteConcepts(ds);
		}
		return clashfound;
	}
	
	
	/**
	 * 1. find clashes 
	 * for each pair with the same feature, e.g, f=k1, g<k2, h<=k3, look for the clashes.
	 * true if any clash
	 * @param cs
	 * @return
	 */
	public boolean clashConcreteConcepts(HashSet<DomainConcept<?,?>> cs){
		//clear previous results
		//
		FeatureGraph fg = new FeatureGraph();
		fg.buildGraph(cs);
		return fg.clashFinder();
	}
	
	//for all the f feature concepts
	public boolean clashOfEQ(HashSet<DomainConcept<?,?>> dcs){
		HashMap<Object, HashSet<Object>> fmap = this.computeTransitiveClosure(dcs, 
				new HashMap<Object, HashSet<Object>>());
		for(Object f:fmap.keySet()){
			//if f =k1 and f=k2 and k1!=k2, then clash
			if(fmap.get(f).size()<2){
				continue;
			}
			int count = 0;
			for(Object o:fmap.get(f)){
				if(o instanceof String){
					count++;
				}
				if(count > 1){
					//two values for the same feature!
					return false;
				}
			}
		}
		return true;
	}
	
	public boolean clashOfLT(HashSet <DomainConcept<?,?>> lt){
		HashMap<Object, HashSet<Object>> fmap = this.computeTransitiveClosure(lt, 
				new HashMap<Object, HashSet<Object>>());
		for(Object f:fmap.keySet()){
			//if f<f, then unsat!
			if(fmap.get(f).contains(f)){
				return false;
			}
		}
		return true;
	}
	/*
	 * Only consider ?<?, ?<=?
	 */
	public HashMap<Object, HashSet<Object>> computeTransitiveClosure(HashSet<DomainConcept<?,?>> ds, 
			HashMap<Object, HashSet<Object>> map){
		boolean update = false;
		for(DomainConcept<?,?> dc:ds){
			/*if(!(dc instanceof DomainConceptLT) && !(dc instanceof DomainConceptLTEQ)){
				//not considered
				continue;
			}*/
			Object f = dc.getFeature();
			Object g = dc.getValue();
			if(map.containsKey(f)){
				if(!map.get(f).contains(g)){
					map.get(f).add(g);
					if(map.containsKey(g)){
						map.get(f).addAll(map.get(g));
					}
					update |= true;
				}
			}else{
				update |= true;
				map.put(f, new HashSet<Object>());
				map.get(f).add(g);
				if(map.containsKey(g)){
					map.get(f).addAll(map.get(g));
				}
			}
		}
		//if any update to any entry, then update the whole map
		if(update){
			map = this.saturation(map);
		}		
		return map;
	}
	
	//a simple recursion to compute transitive closure.
	public HashMap<Object, HashSet<Object>> saturation(HashMap<Object, HashSet<Object>> map){
		boolean update = false;
		for(Object f:map.keySet()){
			HashSet<Object> ds = map.get(f);
			int size1 = ds.size();
			if(ds.size()<1){
				continue;
			}
			for(Object g:ds){
				if(map.containsKey(g)){
					map.get(f).addAll(map.get(g));
				}
			}
			//if set enlarged -> true
			update |= size1 < map.get(f).size();
		}
		if(update){
			map = saturation(map);
		}
		return map;
	}
	
}
